5.3 PAT Extensions

5.3 PAT Extensions

In this section, we discuss the possible extensions of PAT with the help of the pre-defined APIs, examples and libraries. These extensions allow domain experts to create customized model checkers in all levels, based on their knowledge of the model checking.

Basically, we will introduce how to create a dedicated model checker by means of following four ways which will be covered in detail in four sub-sections respectively.

Language Translation: Translating models into a language supported by an existing module in PAT through the module APIs.
Language Extension: Extending one of the existing languages with new syntax, data types or libraries.
Algorithm Extension: Extending PAT with general or domain specific new model checking algorithms, state reduction techniques or abstraction techniques.
Module Extension: Extending PAT with a completely new module supporting a new language.

After reading over all the four methods, you will be skilled to develop your own model checker. Have fun!